Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
U13(tt) → tt
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt, V1, V2) → U82(isNatKind(V1), V1, V2)
U82(tt, V1, V2) → U83(isNatIListKind(V2), V1, V2)
U83(tt, V1, V2) → U84(isNatIListKind(V2), V1, V2)
U84(tt, V1, V2) → U85(isNat(V1), V2)
U85(tt, V2) → U86(isNatList(V2))
U86(tt) → tt
U91(tt, L, N) → U92(isNatIListKind(L), L, N)
U92(tt, L, N) → U93(isNat(N), L, N)
U93(tt, L, N) → U94(isNatKind(N), L)
U94(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
isNatKind(s(V1)) → U71(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U81(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U91(isNatList(L), L, N)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
U12: {1}
isNatIListKind: empty set
U13: {1}
isNatList: empty set
U21: {1}
U22: {1}
isNatKind: empty set
U23: {1}
isNat: empty set
U31: {1}
U32: {1}
U33: {1}
U41: {1}
U42: {1}
U43: {1}
U44: {1}
U45: {1}
U46: {1}
isNatIList: empty set
U51: {1}
U52: {1}
U61: {1}
U71: {1}
U81: {1}
U82: {1}
U83: {1}
U84: {1}
U85: {1}
U86: {1}
U91: {1}
U92: {1}
U93: {1}
U94: {1}
s: {1}
length: {1}
nil: empty set


↳ CSR
  ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
U13(tt) → tt
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt, V1, V2) → U82(isNatKind(V1), V1, V2)
U82(tt, V1, V2) → U83(isNatIListKind(V2), V1, V2)
U83(tt, V1, V2) → U84(isNatIListKind(V2), V1, V2)
U84(tt, V1, V2) → U85(isNat(V1), V2)
U85(tt, V2) → U86(isNatList(V2))
U86(tt) → tt
U91(tt, L, N) → U92(isNatIListKind(L), L, N)
U92(tt, L, N) → U93(isNat(N), L, N)
U93(tt, L, N) → U94(isNatKind(N), L)
U94(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
isNatKind(s(V1)) → U71(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U81(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U91(isNatList(L), L, N)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
U12: {1}
isNatIListKind: empty set
U13: {1}
isNatList: empty set
U21: {1}
U22: {1}
isNatKind: empty set
U23: {1}
isNat: empty set
U31: {1}
U32: {1}
U33: {1}
U41: {1}
U42: {1}
U43: {1}
U44: {1}
U45: {1}
U46: {1}
isNatIList: empty set
U51: {1}
U52: {1}
U61: {1}
U71: {1}
U81: {1}
U82: {1}
U83: {1}
U84: {1}
U85: {1}
U86: {1}
U91: {1}
U92: {1}
U93: {1}
U94: {1}
s: {1}
length: {1}
nil: empty set

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U13, U23, U33, U46, U52, U61, U71, U86, s, length, U131, U231, U331, U461, U521, U861, LENGTH, U611, U711} are replacing on all positions.
For all symbols f in {cons, U11, U12, U21, U22, U31, U32, U41, U42, U43, U44, U45, U51, U81, U82, U83, U84, U85, U91, U92, U93, U94, U121, U111, U221, U211, U321, U311, U421, U411, U431, U441, U451, U511, U821, U811, U831, U841, U851, U921, U911, U931, U941} we have µ(f) = {1}.
The symbols in {isNatIListKind, isNatList, isNatKind, isNat, isNatIList, ISNATILISTKIND, ISNATLIST, ISNATKIND, ISNAT, ISNATILIST, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

U111(tt, V1) → U121(isNatIListKind(V1), V1)
U111(tt, V1) → ISNATILISTKIND(V1)
U121(tt, V1) → U131(isNatList(V1))
U121(tt, V1) → ISNATLIST(V1)
U211(tt, V1) → U221(isNatKind(V1), V1)
U211(tt, V1) → ISNATKIND(V1)
U221(tt, V1) → U231(isNat(V1))
U221(tt, V1) → ISNAT(V1)
U311(tt, V) → U321(isNatIListKind(V), V)
U311(tt, V) → ISNATILISTKIND(V)
U321(tt, V) → U331(isNatList(V))
U321(tt, V) → ISNATLIST(V)
U411(tt, V1, V2) → U421(isNatKind(V1), V1, V2)
U411(tt, V1, V2) → ISNATKIND(V1)
U421(tt, V1, V2) → U431(isNatIListKind(V2), V1, V2)
U421(tt, V1, V2) → ISNATILISTKIND(V2)
U431(tt, V1, V2) → U441(isNatIListKind(V2), V1, V2)
U431(tt, V1, V2) → ISNATILISTKIND(V2)
U441(tt, V1, V2) → U451(isNat(V1), V2)
U441(tt, V1, V2) → ISNAT(V1)
U451(tt, V2) → U461(isNatIList(V2))
U451(tt, V2) → ISNATILIST(V2)
U511(tt, V2) → U521(isNatIListKind(V2))
U511(tt, V2) → ISNATILISTKIND(V2)
U811(tt, V1, V2) → U821(isNatKind(V1), V1, V2)
U811(tt, V1, V2) → ISNATKIND(V1)
U821(tt, V1, V2) → U831(isNatIListKind(V2), V1, V2)
U821(tt, V1, V2) → ISNATILISTKIND(V2)
U831(tt, V1, V2) → U841(isNatIListKind(V2), V1, V2)
U831(tt, V1, V2) → ISNATILISTKIND(V2)
U841(tt, V1, V2) → U851(isNat(V1), V2)
U841(tt, V1, V2) → ISNAT(V1)
U851(tt, V2) → U861(isNatList(V2))
U851(tt, V2) → ISNATLIST(V2)
U911(tt, L, N) → U921(isNatIListKind(L), L, N)
U911(tt, L, N) → ISNATILISTKIND(L)
U921(tt, L, N) → U931(isNat(N), L, N)
U921(tt, L, N) → ISNAT(N)
U931(tt, L, N) → U941(isNatKind(N), L)
U931(tt, L, N) → ISNATKIND(N)
U941(tt, L) → LENGTH(L)
ISNAT(length(V1)) → U111(isNatIListKind(V1), V1)
ISNAT(length(V1)) → ISNATILISTKIND(V1)
ISNAT(s(V1)) → U211(isNatKind(V1), V1)
ISNAT(s(V1)) → ISNATKIND(V1)
ISNATILIST(V) → U311(isNatIListKind(V), V)
ISNATILIST(V) → ISNATILISTKIND(V)
ISNATILIST(cons(V1, V2)) → U411(isNatKind(V1), V1, V2)
ISNATILIST(cons(V1, V2)) → ISNATKIND(V1)
ISNATILISTKIND(cons(V1, V2)) → U511(isNatKind(V1), V2)
ISNATILISTKIND(cons(V1, V2)) → ISNATKIND(V1)
ISNATKIND(length(V1)) → U611(isNatIListKind(V1))
ISNATKIND(length(V1)) → ISNATILISTKIND(V1)
ISNATKIND(s(V1)) → U711(isNatKind(V1))
ISNATKIND(s(V1)) → ISNATKIND(V1)
ISNATLIST(cons(V1, V2)) → U811(isNatKind(V1), V1, V2)
ISNATLIST(cons(V1, V2)) → ISNATKIND(V1)
LENGTH(cons(N, L)) → U911(isNatList(L), L, N)
LENGTH(cons(N, L)) → ISNATLIST(L)

The collapsing dependency pairs are DPc:

U941(tt, L) → L


The hidden terms of R are:

zeros

Every hiding context is built from:none

Hence, the new unhiding pairs DPu are :

U941(tt, L) → U(L)
U(zeros) → ZEROS

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
U13(tt) → tt
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt, V1, V2) → U82(isNatKind(V1), V1, V2)
U82(tt, V1, V2) → U83(isNatIListKind(V2), V1, V2)
U83(tt, V1, V2) → U84(isNatIListKind(V2), V1, V2)
U84(tt, V1, V2) → U85(isNat(V1), V2)
U85(tt, V2) → U86(isNatList(V2))
U86(tt) → tt
U91(tt, L, N) → U92(isNatIListKind(L), L, N)
U92(tt, L, N) → U93(isNat(N), L, N)
U93(tt, L, N) → U94(isNatKind(N), L)
U94(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
isNatKind(s(V1)) → U71(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U81(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U91(isNatList(L), L, N)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 4 SCCs with 32 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U13, U23, U33, U46, U52, U61, U71, U86, s, length} are replacing on all positions.
For all symbols f in {cons, U11, U12, U21, U22, U31, U32, U41, U42, U43, U44, U45, U51, U81, U82, U83, U84, U85, U91, U92, U93, U94, U511} we have µ(f) = {1}.
The symbols in {isNatIListKind, isNatList, isNatKind, isNat, isNatIList, ISNATILISTKIND, ISNATKIND} are not replacing on any position.

The TRS P consists of the following rules:

U511(tt, V2) → ISNATILISTKIND(V2)
ISNATILISTKIND(cons(V1, V2)) → U511(isNatKind(V1), V2)
ISNATILISTKIND(cons(V1, V2)) → ISNATKIND(V1)
ISNATKIND(length(V1)) → ISNATILISTKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
U13(tt) → tt
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt, V1, V2) → U82(isNatKind(V1), V1, V2)
U82(tt, V1, V2) → U83(isNatIListKind(V2), V1, V2)
U83(tt, V1, V2) → U84(isNatIListKind(V2), V1, V2)
U84(tt, V1, V2) → U85(isNat(V1), V2)
U85(tt, V2) → U86(isNatList(V2))
U86(tt) → tt
U91(tt, L, N) → U92(isNatIListKind(L), L, N)
U92(tt, L, N) → U93(isNat(N), L, N)
U93(tt, L, N) → U94(isNatKind(N), L)
U94(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
isNatKind(s(V1)) → U71(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U81(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U91(isNatList(L), L, N)

Q is empty.

The following rules are not useable and can be deleted:

zeros → cons(0, zeros)
U11(tt, x0) → U12(isNatIListKind(x0), x0)
U12(tt, x0) → U13(isNatList(x0))
U13(tt) → tt
U21(tt, x0) → U22(isNatKind(x0), x0)
U22(tt, x0) → U23(isNat(x0))
U23(tt) → tt
U31(tt, x0) → U32(isNatIListKind(x0), x0)
U32(tt, x0) → U33(isNatList(x0))
U33(tt) → tt
U41(tt, x0, x1) → U42(isNatKind(x0), x0, x1)
U42(tt, x0, x1) → U43(isNatIListKind(x1), x0, x1)
U43(tt, x0, x1) → U44(isNatIListKind(x1), x0, x1)
U44(tt, x0, x1) → U45(isNat(x0), x1)
U45(tt, x0) → U46(isNatIList(x0))
U46(tt) → tt
U81(tt, x0, x1) → U82(isNatKind(x0), x0, x1)
U82(tt, x0, x1) → U83(isNatIListKind(x1), x0, x1)
U83(tt, x0, x1) → U84(isNatIListKind(x1), x0, x1)
U84(tt, x0, x1) → U85(isNat(x0), x1)
U85(tt, x0) → U86(isNatList(x0))
U86(tt) → tt
U91(tt, x0, x1) → U92(isNatIListKind(x0), x0, x1)
U92(tt, x0, x1) → U93(isNat(x1), x0, x1)
U93(tt, x0, x1) → U94(isNatKind(x1), x0)
U94(tt, x0) → s(length(x0))
isNat(0) → tt
isNat(length(x0)) → U11(isNatIListKind(x0), x0)
isNat(s(x0)) → U21(isNatKind(x0), x0)
isNatIList(x0) → U31(isNatIListKind(x0), x0)
isNatIList(zeros) → tt
isNatIList(cons(x0, x1)) → U41(isNatKind(x0), x0, x1)
isNatList(nil) → tt
isNatList(cons(x0, x1)) → U81(isNatKind(x0), x0, x1)
length(nil) → 0
length(cons(x0, x1)) → U91(isNatList(x1), x1, x0)


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U61, s, U71, U52} are replacing on all positions.
For all symbols f in {cons, U51, U511} we have µ(f) = {1}.
The symbols in {isNatKind, isNatIListKind, ISNATILISTKIND, ISNATKIND} are not replacing on any position.

The TRS P consists of the following rules:

U511(tt, V2) → ISNATILISTKIND(V2)
ISNATILISTKIND(cons(V1, V2)) → U511(isNatKind(V1), V2)
ISNATILISTKIND(cons(V1, V2)) → ISNATKIND(V1)
ISNATKIND(length(V1)) → ISNATILISTKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)

The TRS R consists of the following rules:

isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(s(V1)) → U71(isNatKind(V1))
U71(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt) → tt

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 2   
POL(ISNATILISTKIND(x1)) = 1 + 2·x1   
POL(ISNATKIND(x1)) = 2 + x1   
POL(U51(x1, x2)) = 1 + 2·x2   
POL(U511(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(U52(x1)) = 1 + 2·x1   
POL(U61(x1)) = 2 + x1   
POL(U71(x1)) = 1 + 2·x1   
POL(cons(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(isNatIListKind(x1)) = x1   
POL(isNatKind(x1)) = x1   
POL(length(x1)) = 2 + 2·x1   
POL(nil) = 2   
POL(s(x1)) = 1 + 2·x1   
POL(tt) = 2   
POL(zeros) = 2   

the following usable rules

isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
isNatKind(s(V1)) → U71(isNatKind(V1))
U61(tt) → tt
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U71(tt) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

U511(tt, V2) → ISNATILISTKIND(V2)
ISNATILISTKIND(cons(V1, V2)) → U511(isNatKind(V1), V2)
ISNATILISTKIND(cons(V1, V2)) → ISNATKIND(V1)
ISNATKIND(length(V1)) → ISNATILISTKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)

could be oriented strictly and thus removed.
All pairs have been removed.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                  ↳ QCSDP
                    ↳ PIsEmptyProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U61, s, U71, U52} are replacing on all positions.
For all symbols f in {cons, U51} we have µ(f) = {1}.
The symbols in {isNatKind, isNatIListKind} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(s(V1)) → U71(isNatKind(V1))
U71(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt) → tt

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U13, U23, U33, U46, U52, U61, U71, U86, s, length} are replacing on all positions.
For all symbols f in {cons, U11, U12, U21, U22, U31, U32, U41, U42, U43, U44, U45, U51, U81, U82, U83, U84, U85, U91, U92, U93, U94, U121, U811, U821, U831, U841, U851, U111, U211, U221} we have µ(f) = {1}.
The symbols in {isNatIListKind, isNatList, isNatKind, isNat, isNatIList, ISNATLIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

U121(tt, V1) → ISNATLIST(V1)
ISNATLIST(cons(V1, V2)) → U811(isNatKind(V1), V1, V2)
U811(tt, V1, V2) → U821(isNatKind(V1), V1, V2)
U821(tt, V1, V2) → U831(isNatIListKind(V2), V1, V2)
U831(tt, V1, V2) → U841(isNatIListKind(V2), V1, V2)
U841(tt, V1, V2) → U851(isNat(V1), V2)
U851(tt, V2) → ISNATLIST(V2)
U841(tt, V1, V2) → ISNAT(V1)
ISNAT(length(V1)) → U111(isNatIListKind(V1), V1)
U111(tt, V1) → U121(isNatIListKind(V1), V1)
ISNAT(s(V1)) → U211(isNatKind(V1), V1)
U211(tt, V1) → U221(isNatKind(V1), V1)
U221(tt, V1) → ISNAT(V1)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
U13(tt) → tt
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt, V1, V2) → U82(isNatKind(V1), V1, V2)
U82(tt, V1, V2) → U83(isNatIListKind(V2), V1, V2)
U83(tt, V1, V2) → U84(isNatIListKind(V2), V1, V2)
U84(tt, V1, V2) → U85(isNat(V1), V2)
U85(tt, V2) → U86(isNatList(V2))
U86(tt) → tt
U91(tt, L, N) → U92(isNatIListKind(L), L, N)
U92(tt, L, N) → U93(isNat(N), L, N)
U93(tt, L, N) → U94(isNatKind(N), L)
U94(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
isNatKind(s(V1)) → U71(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U81(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U91(isNatList(L), L, N)

Q is empty.

The following rules are not useable and can be deleted:

zeros → cons(0, zeros)
U31(tt, x0) → U32(isNatIListKind(x0), x0)
U32(tt, x0) → U33(isNatList(x0))
U33(tt) → tt
U41(tt, x0, x1) → U42(isNatKind(x0), x0, x1)
U42(tt, x0, x1) → U43(isNatIListKind(x1), x0, x1)
U43(tt, x0, x1) → U44(isNatIListKind(x1), x0, x1)
U44(tt, x0, x1) → U45(isNat(x0), x1)
U45(tt, x0) → U46(isNatIList(x0))
U46(tt) → tt
U91(tt, x0, x1) → U92(isNatIListKind(x0), x0, x1)
U92(tt, x0, x1) → U93(isNat(x1), x0, x1)
U93(tt, x0, x1) → U94(isNatKind(x1), x0)
U94(tt, x0) → s(length(x0))
isNatIList(x0) → U31(isNatIListKind(x0), x0)
isNatIList(zeros) → tt
isNatIList(cons(x0, x1)) → U41(isNatKind(x0), x0, x1)
length(nil) → 0
length(cons(x0, x1)) → U91(isNatList(x1), x1, x0)


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U61, s, U71, U52, U13, U23, U86} are replacing on all positions.
For all symbols f in {cons, U51, U11, U12, U81, U82, U83, U84, U85, U21, U22, U121, U811, U821, U831, U841, U851, U111, U211, U221} we have µ(f) = {1}.
The symbols in {isNatKind, isNatIListKind, isNat, isNatList, ISNATLIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

U121(tt, V1) → ISNATLIST(V1)
ISNATLIST(cons(V1, V2)) → U811(isNatKind(V1), V1, V2)
U811(tt, V1, V2) → U821(isNatKind(V1), V1, V2)
U821(tt, V1, V2) → U831(isNatIListKind(V2), V1, V2)
U831(tt, V1, V2) → U841(isNatIListKind(V2), V1, V2)
U841(tt, V1, V2) → U851(isNat(V1), V2)
U851(tt, V2) → ISNATLIST(V2)
U841(tt, V1, V2) → ISNAT(V1)
ISNAT(length(V1)) → U111(isNatIListKind(V1), V1)
U111(tt, V1) → U121(isNatIListKind(V1), V1)
ISNAT(s(V1)) → U211(isNatKind(V1), V1)
U211(tt, V1) → U221(isNatKind(V1), V1)
U221(tt, V1) → ISNAT(V1)

The TRS R consists of the following rules:

isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(s(V1)) → U71(isNatKind(V1))
U71(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U81(isNatKind(V1), V1, V2)
U81(tt, V1, V2) → U82(isNatKind(V1), V1, V2)
U82(tt, V1, V2) → U83(isNatIListKind(V2), V1, V2)
U83(tt, V1, V2) → U84(isNatIListKind(V2), V1, V2)
U84(tt, V1, V2) → U85(isNat(V1), V2)
isNat(s(V1)) → U21(isNatKind(V1), V1)
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U85(tt, V2) → U86(isNatList(V2))
U86(tt) → tt
U13(tt) → tt

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 1   
POL(ISNAT(x1)) = 2·x1   
POL(ISNATLIST(x1)) = x1   
POL(U11(x1, x2)) = 2·x1 + x2   
POL(U111(x1, x2)) = x2   
POL(U12(x1, x2)) = 2·x1   
POL(U121(x1, x2)) = x2   
POL(U13(x1)) = 2·x1   
POL(U21(x1, x2)) = 2·x1 + x2   
POL(U211(x1, x2)) = 2·x1 + 2·x2   
POL(U22(x1, x2)) = x2   
POL(U221(x1, x2)) = 2·x1 + 2·x2   
POL(U23(x1)) = 0   
POL(U51(x1, x2)) = 0   
POL(U52(x1)) = 0   
POL(U61(x1)) = 2·x1   
POL(U71(x1)) = x1   
POL(U81(x1, x2, x3)) = x1   
POL(U811(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U82(x1, x2, x3)) = 0   
POL(U821(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3   
POL(U83(x1, x2, x3)) = 0   
POL(U831(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U84(x1, x2, x3)) = 0   
POL(U841(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U85(x1, x2)) = 0   
POL(U851(x1, x2)) = x2   
POL(U86(x1)) = 2·x1   
POL(cons(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(isNat(x1)) = 2·x1   
POL(isNatIListKind(x1)) = 0   
POL(isNatKind(x1)) = 0   
POL(isNatList(x1)) = 0   
POL(length(x1)) = 2·x1   
POL(nil) = 2   
POL(s(x1)) = 1 + x1   
POL(tt) = 0   
POL(zeros) = 0   

the following usable rules

isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
isNatKind(s(V1)) → U71(isNatKind(V1))
U61(tt) → tt
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U71(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
U13(tt) → tt
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U81(isNatKind(V1), V1, V2)
U81(tt, V1, V2) → U82(isNatKind(V1), V1, V2)
U82(tt, V1, V2) → U83(isNatIListKind(V2), V1, V2)
U83(tt, V1, V2) → U84(isNatIListKind(V2), V1, V2)
U84(tt, V1, V2) → U85(isNat(V1), V2)
U85(tt, V2) → U86(isNatList(V2))
U86(tt) → tt
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

ISNATLIST(cons(V1, V2)) → U811(isNatKind(V1), V1, V2)
ISNAT(s(V1)) → U211(isNatKind(V1), V1)

could be oriented strictly and thus removed.
The pairs

U121(tt, V1) → ISNATLIST(V1)
U811(tt, V1, V2) → U821(isNatKind(V1), V1, V2)
U821(tt, V1, V2) → U831(isNatIListKind(V2), V1, V2)
U831(tt, V1, V2) → U841(isNatIListKind(V2), V1, V2)
U841(tt, V1, V2) → U851(isNat(V1), V2)
U851(tt, V2) → ISNATLIST(V2)
U841(tt, V1, V2) → ISNAT(V1)
ISNAT(length(V1)) → U111(isNatIListKind(V1), V1)
U111(tt, V1) → U121(isNatIListKind(V1), V1)
U211(tt, V1) → U221(isNatKind(V1), V1)
U221(tt, V1) → ISNAT(V1)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U61, s, U71, U52, U13, U23, U86} are replacing on all positions.
For all symbols f in {cons, U51, U11, U12, U81, U82, U83, U84, U85, U21, U22, U121, U821, U811, U831, U841, U851, U111, U221, U211} we have µ(f) = {1}.
The symbols in {isNatKind, isNatIListKind, isNat, isNatList, ISNATLIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

U121(tt, V1) → ISNATLIST(V1)
U811(tt, V1, V2) → U821(isNatKind(V1), V1, V2)
U821(tt, V1, V2) → U831(isNatIListKind(V2), V1, V2)
U831(tt, V1, V2) → U841(isNatIListKind(V2), V1, V2)
U841(tt, V1, V2) → U851(isNat(V1), V2)
U851(tt, V2) → ISNATLIST(V2)
U841(tt, V1, V2) → ISNAT(V1)
ISNAT(length(V1)) → U111(isNatIListKind(V1), V1)
U111(tt, V1) → U121(isNatIListKind(V1), V1)
U211(tt, V1) → U221(isNatKind(V1), V1)
U221(tt, V1) → ISNAT(V1)

The TRS R consists of the following rules:

isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(s(V1)) → U71(isNatKind(V1))
U71(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U81(isNatKind(V1), V1, V2)
U81(tt, V1, V2) → U82(isNatKind(V1), V1, V2)
U82(tt, V1, V2) → U83(isNatIListKind(V2), V1, V2)
U83(tt, V1, V2) → U84(isNatIListKind(V2), V1, V2)
U84(tt, V1, V2) → U85(isNat(V1), V2)
isNat(s(V1)) → U21(isNatKind(V1), V1)
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U85(tt, V2) → U86(isNatList(V2))
U86(tt) → tt
U13(tt) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 11 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPReductionPairProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U13, U23, U33, U46, U52, U61, U71, U86, s, length, LENGTH} are replacing on all positions.
For all symbols f in {cons, U11, U12, U21, U22, U31, U32, U41, U42, U43, U44, U45, U51, U81, U82, U83, U84, U85, U91, U92, U93, U94, U911, U921, U931, U941} we have µ(f) = {1}.
The symbols in {isNatIListKind, isNatList, isNatKind, isNat, isNatIList} are not replacing on any position.

The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U911(isNatList(L), L, N)
U911(tt, L, N) → U921(isNatIListKind(L), L, N)
U921(tt, L, N) → U931(isNat(N), L, N)
U931(tt, L, N) → U941(isNatKind(N), L)
U941(tt, L) → LENGTH(L)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
U13(tt) → tt
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt, V1, V2) → U82(isNatKind(V1), V1, V2)
U82(tt, V1, V2) → U83(isNatIListKind(V2), V1, V2)
U83(tt, V1, V2) → U84(isNatIListKind(V2), V1, V2)
U84(tt, V1, V2) → U85(isNat(V1), V2)
U85(tt, V2) → U86(isNatList(V2))
U86(tt) → tt
U91(tt, L, N) → U92(isNatIListKind(L), L, N)
U92(tt, L, N) → U93(isNat(N), L, N)
U93(tt, L, N) → U94(isNatKind(N), L)
U94(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
isNatKind(s(V1)) → U71(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U81(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U91(isNatList(L), L, N)

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 1   
POL(LENGTH(x1)) = 2·x1   
POL(U11(x1, x2)) = 1   
POL(U12(x1, x2)) = 1   
POL(U13(x1)) = 1   
POL(U21(x1, x2)) = 2   
POL(U22(x1, x2)) = 2   
POL(U23(x1)) = 1   
POL(U51(x1, x2)) = 2   
POL(U52(x1)) = 1   
POL(U61(x1)) = 2·x1   
POL(U71(x1)) = 1   
POL(U81(x1, x2, x3)) = x3   
POL(U82(x1, x2, x3)) = x3   
POL(U83(x1, x2, x3)) = x3   
POL(U84(x1, x2, x3)) = x3   
POL(U85(x1, x2)) = x2   
POL(U86(x1)) = x1   
POL(U91(x1, x2, x3)) = 2 + 2·x1   
POL(U911(x1, x2, x3)) = 2·x1 + 2·x2   
POL(U92(x1, x2, x3)) = 1 + x1   
POL(U921(x1, x2, x3)) = 1 + 2·x2   
POL(U93(x1, x2, x3)) = 1   
POL(U931(x1, x2, x3)) = 2·x2   
POL(U94(x1, x2)) = 1   
POL(U941(x1, x2)) = 2·x2   
POL(cons(x1, x2)) = 2·x2   
POL(isNat(x1)) = 2   
POL(isNatIListKind(x1)) = 2   
POL(isNatKind(x1)) = 2·x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 2 + 2·x1   
POL(nil) = 1   
POL(s(x1)) = 1   
POL(tt) = 1   
POL(zeros) = 0   

the following usable rules

isNatList(nil) → tt
isNatList(cons(V1, V2)) → U81(isNatKind(V1), V1, V2)
U81(tt, V1, V2) → U82(isNatKind(V1), V1, V2)
U82(tt, V1, V2) → U83(isNatIListKind(V2), V1, V2)
U83(tt, V1, V2) → U84(isNatIListKind(V2), V1, V2)
U84(tt, V1, V2) → U85(isNat(V1), V2)
U85(tt, V2) → U86(isNatList(V2))
U86(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
length(nil) → 0
length(cons(N, L)) → U91(isNatList(L), L, N)
U91(tt, L, N) → U92(isNatIListKind(L), L, N)
U92(tt, L, N) → U93(isNat(N), L, N)
U93(tt, L, N) → U94(isNatKind(N), L)
U94(tt, L) → s(length(L))
isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
isNatKind(s(V1)) → U71(isNatKind(V1))
U61(tt) → tt
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
zeros → cons(0, zeros)
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U71(tt) → tt
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
U13(tt) → tt
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt

could all be oriented weakly.
Furthermore, the pairs

U911(tt, L, N) → U921(isNatIListKind(L), L, N)
U921(tt, L, N) → U931(isNat(N), L, N)

could be oriented strictly and thus removed.
The pairs

LENGTH(cons(N, L)) → U911(isNatList(L), L, N)
U931(tt, L, N) → U941(isNatKind(N), L)
U941(tt, L) → LENGTH(L)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPReductionPairProof
              ↳ QCSDP
                ↳ QCSDependencyGraphProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U13, U23, U33, U46, U52, U61, U71, U86, s, length, LENGTH} are replacing on all positions.
For all symbols f in {cons, U11, U12, U21, U22, U31, U32, U41, U42, U43, U44, U45, U51, U81, U82, U83, U84, U85, U91, U92, U93, U94, U911, U941, U931} we have µ(f) = {1}.
The symbols in {isNatIListKind, isNatList, isNatKind, isNat, isNatIList} are not replacing on any position.

The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U911(isNatList(L), L, N)
U931(tt, L, N) → U941(isNatKind(N), L)
U941(tt, L) → LENGTH(L)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
U13(tt) → tt
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt, V1, V2) → U82(isNatKind(V1), V1, V2)
U82(tt, V1, V2) → U83(isNatIListKind(V2), V1, V2)
U83(tt, V1, V2) → U84(isNatIListKind(V2), V1, V2)
U84(tt, V1, V2) → U85(isNat(V1), V2)
U85(tt, V2) → U86(isNatList(V2))
U86(tt) → tt
U91(tt, L, N) → U92(isNatIListKind(L), L, N)
U92(tt, L, N) → U93(isNat(N), L, N)
U93(tt, L, N) → U94(isNatKind(N), L)
U94(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
isNatKind(s(V1)) → U71(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U81(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U91(isNatList(L), L, N)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 3 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U13, U23, U33, U46, U52, U61, U71, U86, s, length} are replacing on all positions.
For all symbols f in {cons, U11, U12, U21, U22, U31, U32, U41, U42, U43, U44, U45, U51, U81, U82, U83, U84, U85, U91, U92, U93, U94, U451, U441, U411, U421, U431} we have µ(f) = {1}.
The symbols in {isNatIListKind, isNatList, isNatKind, isNat, isNatIList, ISNATILIST} are not replacing on any position.

The TRS P consists of the following rules:

U441(tt, V1, V2) → U451(isNat(V1), V2)
U451(tt, V2) → ISNATILIST(V2)
ISNATILIST(cons(V1, V2)) → U411(isNatKind(V1), V1, V2)
U411(tt, V1, V2) → U421(isNatKind(V1), V1, V2)
U421(tt, V1, V2) → U431(isNatIListKind(V2), V1, V2)
U431(tt, V1, V2) → U441(isNatIListKind(V2), V1, V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
U13(tt) → tt
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V) → U32(isNatIListKind(V), V)
U32(tt, V) → U33(isNatList(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isNatKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isNatIListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isNatIListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isNat(V1), V2)
U45(tt, V2) → U46(isNatIList(V2))
U46(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt, V1, V2) → U82(isNatKind(V1), V1, V2)
U82(tt, V1, V2) → U83(isNatIListKind(V2), V1, V2)
U83(tt, V1, V2) → U84(isNatIListKind(V2), V1, V2)
U84(tt, V1, V2) → U85(isNat(V1), V2)
U85(tt, V2) → U86(isNatList(V2))
U86(tt) → tt
U91(tt, L, N) → U92(isNatIListKind(L), L, N)
U92(tt, L, N) → U93(isNat(N), L, N)
U93(tt, L, N) → U94(isNatKind(N), L)
U94(tt, L) → s(length(L))
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNatKind(V1), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
isNatKind(s(V1)) → U71(isNatKind(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U81(isNatKind(V1), V1, V2)
length(nil) → 0
length(cons(N, L)) → U91(isNatList(L), L, N)

Q is empty.

The following rules are not useable and can be deleted:

zeros → cons(0, zeros)
U31(tt, x0) → U32(isNatIListKind(x0), x0)
U32(tt, x0) → U33(isNatList(x0))
U33(tt) → tt
U41(tt, x0, x1) → U42(isNatKind(x0), x0, x1)
U42(tt, x0, x1) → U43(isNatIListKind(x1), x0, x1)
U43(tt, x0, x1) → U44(isNatIListKind(x1), x0, x1)
U44(tt, x0, x1) → U45(isNat(x0), x1)
U45(tt, x0) → U46(isNatIList(x0))
U46(tt) → tt
U91(tt, x0, x1) → U92(isNatIListKind(x0), x0, x1)
U92(tt, x0, x1) → U93(isNat(x1), x0, x1)
U93(tt, x0, x1) → U94(isNatKind(x1), x0)
U94(tt, x0) → s(length(x0))
isNatIList(x0) → U31(isNatIListKind(x0), x0)
isNatIList(zeros) → tt
isNatIList(cons(x0, x1)) → U41(isNatKind(x0), x0, x1)
length(nil) → 0
length(cons(x0, x1)) → U91(isNatList(x1), x1, x0)


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U61, s, U71, U52, U13, U23, U86} are replacing on all positions.
For all symbols f in {U11, cons, U51, U12, U81, U82, U83, U84, U85, U21, U22, U451, U441, U411, U421, U431} we have µ(f) = {1}.
The symbols in {isNat, isNatIListKind, isNatKind, isNatList, ISNATILIST} are not replacing on any position.

The TRS P consists of the following rules:

U441(tt, V1, V2) → U451(isNat(V1), V2)
U451(tt, V2) → ISNATILIST(V2)
ISNATILIST(cons(V1, V2)) → U411(isNatKind(V1), V1, V2)
U411(tt, V1, V2) → U421(isNatKind(V1), V1, V2)
U421(tt, V1, V2) → U431(isNatIListKind(V2), V1, V2)
U431(tt, V1, V2) → U441(isNatIListKind(V2), V1, V2)

The TRS R consists of the following rules:

isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
U61(tt) → tt
isNatKind(s(V1)) → U71(isNatKind(V1))
U71(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U81(isNatKind(V1), V1, V2)
U81(tt, V1, V2) → U82(isNatKind(V1), V1, V2)
U82(tt, V1, V2) → U83(isNatIListKind(V2), V1, V2)
U83(tt, V1, V2) → U84(isNatIListKind(V2), V1, V2)
U84(tt, V1, V2) → U85(isNat(V1), V2)
isNat(s(V1)) → U21(isNatKind(V1), V1)
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U85(tt, V2) → U86(isNatList(V2))
U86(tt) → tt
U13(tt) → tt

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 2   
POL(ISNATILIST(x1)) = 2·x1   
POL(U11(x1, x2)) = x1 + x2   
POL(U12(x1, x2)) = x1   
POL(U13(x1)) = 0   
POL(U21(x1, x2)) = 0   
POL(U22(x1, x2)) = 0   
POL(U23(x1)) = 0   
POL(U411(x1, x2, x3)) = 1 + x1 + 2·x2 + 2·x3   
POL(U421(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U431(x1, x2, x3)) = x2 + 2·x3   
POL(U441(x1, x2, x3)) = 2·x3   
POL(U451(x1, x2)) = 2·x2   
POL(U51(x1, x2)) = 0   
POL(U52(x1)) = 0   
POL(U61(x1)) = 1 + x1   
POL(U71(x1)) = x1   
POL(U81(x1, x2, x3)) = 2 + x1 + 2·x2   
POL(U82(x1, x2, x3)) = 2·x2   
POL(U83(x1, x2, x3)) = x1 + x2   
POL(U84(x1, x2, x3)) = 2·x1 + x2   
POL(U85(x1, x2)) = 0   
POL(U86(x1)) = 0   
POL(cons(x1, x2)) = 2 + 2·x1 + x2   
POL(isNat(x1)) = x1   
POL(isNatIListKind(x1)) = 0   
POL(isNatKind(x1)) = 2   
POL(isNatList(x1)) = 2·x1   
POL(length(x1)) = 1 + x1   
POL(nil) = 1   
POL(s(x1)) = 2 + 2·x1   
POL(tt) = 0   
POL(zeros) = 0   

the following usable rules

isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
U13(tt) → tt
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U81(isNatKind(V1), V1, V2)
U81(tt, V1, V2) → U82(isNatKind(V1), V1, V2)
U82(tt, V1, V2) → U83(isNatIListKind(V2), V1, V2)
U83(tt, V1, V2) → U84(isNatIListKind(V2), V1, V2)
U84(tt, V1, V2) → U85(isNat(V1), V2)
U85(tt, V2) → U86(isNatList(V2))
U86(tt) → tt
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
isNatKind(s(V1)) → U71(isNatKind(V1))
U61(tt) → tt
U71(tt) → tt
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

ISNATILIST(cons(V1, V2)) → U411(isNatKind(V1), V1, V2)
U411(tt, V1, V2) → U421(isNatKind(V1), V1, V2)

could be oriented strictly and thus removed.
The pairs

U441(tt, V1, V2) → U451(isNat(V1), V2)
U451(tt, V2) → ISNATILIST(V2)
U421(tt, V1, V2) → U431(isNatIListKind(V2), V1, V2)
U431(tt, V1, V2) → U441(isNatIListKind(V2), V1, V2)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U61, s, U71, U52, U13, U23, U86} are replacing on all positions.
For all symbols f in {U11, cons, U51, U12, U81, U82, U83, U84, U85, U21, U22, U451, U441, U431, U421} we have µ(f) = {1}.
The symbols in {isNat, isNatIListKind, isNatKind, isNatList, ISNATILIST} are not replacing on any position.

The TRS P consists of the following rules:

U441(tt, V1, V2) → U451(isNat(V1), V2)
U451(tt, V2) → ISNATILIST(V2)
U421(tt, V1, V2) → U431(isNatIListKind(V2), V1, V2)
U431(tt, V1, V2) → U441(isNatIListKind(V2), V1, V2)

The TRS R consists of the following rules:

isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → U51(isNatKind(V1), V2)
isNatKind(0) → tt
isNatKind(length(V1)) → U61(isNatIListKind(V1))
U61(tt) → tt
isNatKind(s(V1)) → U71(isNatKind(V1))
U71(tt) → tt
U51(tt, V2) → U52(isNatIListKind(V2))
U52(tt) → tt
U11(tt, V1) → U12(isNatIListKind(V1), V1)
U12(tt, V1) → U13(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U81(isNatKind(V1), V1, V2)
U81(tt, V1, V2) → U82(isNatKind(V1), V1, V2)
U82(tt, V1, V2) → U83(isNatIListKind(V2), V1, V2)
U83(tt, V1, V2) → U84(isNatIListKind(V2), V1, V2)
U84(tt, V1, V2) → U85(isNat(V1), V2)
isNat(s(V1)) → U21(isNatKind(V1), V1)
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U85(tt, V2) → U86(isNatList(V2))
U86(tt) → tt
U13(tt) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 4 less nodes.